(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
0(1(2(x1))) → 0(1(3(2(x1))))
0(1(2(x1))) → 0(2(1(0(x1))))
0(1(2(x1))) → 0(2(1(3(x1))))
0(1(2(x1))) → 0(2(2(1(x1))))
0(1(2(x1))) → 0(2(2(1(4(x1)))))
0(1(2(x1))) → 5(1(0(5(2(3(x1))))))
0(2(4(x1))) → 0(2(1(4(3(x1)))))
0(4(2(x1))) → 4(0(2(3(x1))))
0(4(2(x1))) → 4(0(5(5(2(x1)))))
0(0(4(2(x1)))) → 0(0(2(2(3(4(x1))))))
0(1(2(2(x1)))) → 0(2(1(0(2(x1)))))
0(1(2(2(x1)))) → 1(3(0(2(2(x1)))))
0(1(2(4(x1)))) → 0(1(4(2(3(x1)))))
0(1(2(4(x1)))) → 4(0(2(2(1(1(x1))))))
0(1(2(4(x1)))) → 4(0(5(5(2(1(x1))))))
0(1(2(5(x1)))) → 3(5(5(2(1(0(x1))))))
0(1(4(2(x1)))) → 0(5(2(1(4(x1)))))
0(1(5(2(x1)))) → 1(5(0(2(3(x1)))))
0(1(5(2(x1)))) → 0(2(2(1(0(5(x1))))))
0(1(5(2(x1)))) → 5(5(0(2(1(3(x1))))))
0(2(4(2(x1)))) → 0(5(4(3(2(2(x1))))))
0(3(1(2(x1)))) → 0(2(1(3(2(x1)))))
0(3(1(2(x1)))) → 1(0(2(5(3(x1)))))
0(3(1(2(x1)))) → 1(5(0(2(3(x1)))))
0(3(1(2(x1)))) → 3(0(2(2(1(x1)))))
0(3(1(2(x1)))) → 3(2(2(1(0(x1)))))
0(3(1(2(x1)))) → 0(3(2(3(1(3(x1))))))
0(3(4(2(x1)))) → 0(2(2(3(4(x1)))))
5(0(1(2(x1)))) → 1(3(2(5(0(x1)))))
5(0(1(2(x1)))) → 5(0(2(1(3(3(x1))))))
0(1(1(2(5(x1))))) → 5(0(2(5(1(1(x1))))))
0(2(3(4(2(x1))))) → 3(2(2(3(4(0(x1))))))
0(3(1(2(5(x1))))) → 2(3(1(3(0(5(x1))))))
0(3(1(5(2(x1))))) → 0(3(2(5(1(2(x1))))))
0(3(4(1(4(x1))))) → 0(5(3(1(4(4(x1))))))
0(3(5(1(2(x1))))) → 5(5(3(2(1(0(x1))))))
0(4(0(4(2(x1))))) → 4(4(0(0(2(2(x1))))))
0(4(1(1(2(x1))))) → 3(1(4(0(2(1(x1))))))
0(4(1(2(2(x1))))) → 4(1(0(2(2(3(x1))))))
0(4(1(2(5(x1))))) → 3(4(1(0(2(5(x1))))))
0(4(2(1(2(x1))))) → 4(1(3(2(0(2(x1))))))
0(4(2(1(4(x1))))) → 0(2(1(4(4(4(x1))))))
0(4(2(5(2(x1))))) → 5(4(3(2(2(0(x1))))))
0(4(5(1(2(x1))))) → 1(4(2(0(5(5(x1))))))
0(4(5(1(2(x1))))) → 4(0(2(5(1(1(x1))))))
5(0(1(2(2(x1))))) → 5(0(2(2(1(2(x1))))))
5(0(2(4(2(x1))))) → 0(2(2(5(1(4(x1))))))
5(0(4(4(2(x1))))) → 0(5(2(5(4(4(x1))))))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(1(3(2(z0))))
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(2(2(1(z0))))
0(1(2(z0))) → 0(2(2(1(4(z0)))))
0(1(2(z0))) → 5(1(0(5(2(3(z0))))))
0(2(4(z0))) → 0(2(1(4(3(z0)))))
0(4(2(z0))) → 4(0(2(3(z0))))
0(4(2(z0))) → 4(0(5(5(2(z0)))))
0(0(4(2(z0)))) → 0(0(2(2(3(4(z0))))))
0(1(2(2(z0)))) → 0(2(1(0(2(z0)))))
0(1(2(2(z0)))) → 1(3(0(2(2(z0)))))
0(1(2(4(z0)))) → 0(1(4(2(3(z0)))))
0(1(2(4(z0)))) → 4(0(2(2(1(1(z0))))))
0(1(2(4(z0)))) → 4(0(5(5(2(1(z0))))))
0(1(2(5(z0)))) → 3(5(5(2(1(0(z0))))))
0(1(4(2(z0)))) → 0(5(2(1(4(z0)))))
0(1(5(2(z0)))) → 1(5(0(2(3(z0)))))
0(1(5(2(z0)))) → 0(2(2(1(0(5(z0))))))
0(1(5(2(z0)))) → 5(5(0(2(1(3(z0))))))
0(2(4(2(z0)))) → 0(5(4(3(2(2(z0))))))
0(3(1(2(z0)))) → 0(2(1(3(2(z0)))))
0(3(1(2(z0)))) → 1(0(2(5(3(z0)))))
0(3(1(2(z0)))) → 1(5(0(2(3(z0)))))
0(3(1(2(z0)))) → 3(0(2(2(1(z0)))))
0(3(1(2(z0)))) → 3(2(2(1(0(z0)))))
0(3(1(2(z0)))) → 0(3(2(3(1(3(z0))))))
0(3(4(2(z0)))) → 0(2(2(3(4(z0)))))
0(1(1(2(5(z0))))) → 5(0(2(5(1(1(z0))))))
0(2(3(4(2(z0))))) → 3(2(2(3(4(0(z0))))))
0(3(1(2(5(z0))))) → 2(3(1(3(0(5(z0))))))
0(3(1(5(2(z0))))) → 0(3(2(5(1(2(z0))))))
0(3(4(1(4(z0))))) → 0(5(3(1(4(4(z0))))))
0(3(5(1(2(z0))))) → 5(5(3(2(1(0(z0))))))
0(4(0(4(2(z0))))) → 4(4(0(0(2(2(z0))))))
0(4(1(1(2(z0))))) → 3(1(4(0(2(1(z0))))))
0(4(1(2(2(z0))))) → 4(1(0(2(2(3(z0))))))
0(4(1(2(5(z0))))) → 3(4(1(0(2(5(z0))))))
0(4(2(1(2(z0))))) → 4(1(3(2(0(2(z0))))))
0(4(2(1(4(z0))))) → 0(2(1(4(4(4(z0))))))
0(4(2(5(2(z0))))) → 5(4(3(2(2(0(z0))))))
0(4(5(1(2(z0))))) → 1(4(2(0(5(5(z0))))))
0(4(5(1(2(z0))))) → 4(0(2(5(1(1(z0))))))
5(0(1(2(z0)))) → 1(3(2(5(0(z0)))))
5(0(1(2(z0)))) → 5(0(2(1(3(3(z0))))))
5(0(1(2(2(z0))))) → 5(0(2(2(1(2(z0))))))
5(0(2(4(2(z0))))) → 0(2(2(5(1(4(z0))))))
5(0(4(4(2(z0))))) → 0(5(2(5(4(4(z0))))))
Tuples:
0'(1(2(z0))) → c(0'(1(3(2(z0)))))
0'(1(2(z0))) → c1(0'(2(1(0(z0)))), 0'(z0))
0'(1(2(z0))) → c2(0'(2(1(3(z0)))))
0'(1(2(z0))) → c3(0'(2(2(1(z0)))))
0'(1(2(z0))) → c4(0'(2(2(1(4(z0))))))
0'(1(2(z0))) → c5(5'(1(0(5(2(3(z0)))))), 0'(5(2(3(z0)))), 5'(2(3(z0))))
0'(2(4(z0))) → c6(0'(2(1(4(3(z0))))))
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(4(2(z0))) → c8(0'(5(5(2(z0)))), 5'(5(2(z0))), 5'(2(z0)))
0'(0(4(2(z0)))) → c9(0'(0(2(2(3(4(z0)))))), 0'(2(2(3(4(z0))))))
0'(1(2(2(z0)))) → c10(0'(2(1(0(2(z0))))), 0'(2(z0)))
0'(1(2(2(z0)))) → c11(0'(2(2(z0))))
0'(1(2(4(z0)))) → c12(0'(1(4(2(3(z0))))))
0'(1(2(4(z0)))) → c13(0'(2(2(1(1(z0))))))
0'(1(2(4(z0)))) → c14(0'(5(5(2(1(z0))))), 5'(5(2(1(z0)))), 5'(2(1(z0))))
0'(1(2(5(z0)))) → c15(5'(5(2(1(0(z0))))), 5'(2(1(0(z0)))), 0'(z0))
0'(1(4(2(z0)))) → c16(0'(5(2(1(4(z0))))), 5'(2(1(4(z0)))))
0'(1(5(2(z0)))) → c17(5'(0(2(3(z0)))), 0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(2(2(1(0(5(z0)))))), 0'(5(z0)), 5'(z0))
0'(1(5(2(z0)))) → c19(5'(5(0(2(1(3(z0)))))), 5'(0(2(1(3(z0))))), 0'(2(1(3(z0)))))
0'(2(4(2(z0)))) → c20(0'(5(4(3(2(2(z0)))))), 5'(4(3(2(2(z0))))))
0'(3(1(2(z0)))) → c21(0'(2(1(3(2(z0))))))
0'(3(1(2(z0)))) → c22(0'(2(5(3(z0)))), 5'(3(z0)))
0'(3(1(2(z0)))) → c23(5'(0(2(3(z0)))), 0'(2(3(z0))))
0'(3(1(2(z0)))) → c24(0'(2(2(1(z0)))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(3(1(2(z0)))) → c26(0'(3(2(3(1(3(z0)))))))
0'(3(4(2(z0)))) → c27(0'(2(2(3(4(z0))))))
0'(1(1(2(5(z0))))) → c28(5'(0(2(5(1(1(z0)))))), 0'(2(5(1(1(z0))))), 5'(1(1(z0))))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(3(1(2(5(z0))))) → c30(0'(5(z0)), 5'(z0))
0'(3(1(5(2(z0))))) → c31(0'(3(2(5(1(2(z0)))))), 5'(1(2(z0))))
0'(3(4(1(4(z0))))) → c32(0'(5(3(1(4(4(z0)))))), 5'(3(1(4(4(z0))))))
0'(3(5(1(2(z0))))) → c33(5'(5(3(2(1(0(z0)))))), 5'(3(2(1(0(z0))))), 0'(z0))
0'(4(0(4(2(z0))))) → c34(0'(0(2(2(z0)))), 0'(2(2(z0))))
0'(4(1(1(2(z0))))) → c35(0'(2(1(z0))))
0'(4(1(2(2(z0))))) → c36(0'(2(2(3(z0)))))
0'(4(1(2(5(z0))))) → c37(0'(2(5(z0))), 5'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(4(2(1(4(z0))))) → c39(0'(2(1(4(4(4(z0)))))))
0'(4(2(5(2(z0))))) → c40(5'(4(3(2(2(0(z0)))))), 0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))), 5'(5(z0)), 5'(z0))
0'(4(5(1(2(z0))))) → c42(0'(2(5(1(1(z0))))), 5'(1(1(z0))))
5'(0(1(2(z0)))) → c43(5'(0(z0)), 0'(z0))
5'(0(1(2(z0)))) → c44(5'(0(2(1(3(3(z0)))))), 0'(2(1(3(3(z0))))))
5'(0(1(2(2(z0))))) → c45(5'(0(2(2(1(2(z0)))))), 0'(2(2(1(2(z0))))))
5'(0(2(4(2(z0))))) → c46(0'(2(2(5(1(4(z0)))))), 5'(1(4(z0))))
5'(0(4(4(2(z0))))) → c47(0'(5(2(5(4(4(z0)))))), 5'(2(5(4(4(z0))))), 5'(4(4(z0))))
S tuples:
0'(1(2(z0))) → c(0'(1(3(2(z0)))))
0'(1(2(z0))) → c1(0'(2(1(0(z0)))), 0'(z0))
0'(1(2(z0))) → c2(0'(2(1(3(z0)))))
0'(1(2(z0))) → c3(0'(2(2(1(z0)))))
0'(1(2(z0))) → c4(0'(2(2(1(4(z0))))))
0'(1(2(z0))) → c5(5'(1(0(5(2(3(z0)))))), 0'(5(2(3(z0)))), 5'(2(3(z0))))
0'(2(4(z0))) → c6(0'(2(1(4(3(z0))))))
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(4(2(z0))) → c8(0'(5(5(2(z0)))), 5'(5(2(z0))), 5'(2(z0)))
0'(0(4(2(z0)))) → c9(0'(0(2(2(3(4(z0)))))), 0'(2(2(3(4(z0))))))
0'(1(2(2(z0)))) → c10(0'(2(1(0(2(z0))))), 0'(2(z0)))
0'(1(2(2(z0)))) → c11(0'(2(2(z0))))
0'(1(2(4(z0)))) → c12(0'(1(4(2(3(z0))))))
0'(1(2(4(z0)))) → c13(0'(2(2(1(1(z0))))))
0'(1(2(4(z0)))) → c14(0'(5(5(2(1(z0))))), 5'(5(2(1(z0)))), 5'(2(1(z0))))
0'(1(2(5(z0)))) → c15(5'(5(2(1(0(z0))))), 5'(2(1(0(z0)))), 0'(z0))
0'(1(4(2(z0)))) → c16(0'(5(2(1(4(z0))))), 5'(2(1(4(z0)))))
0'(1(5(2(z0)))) → c17(5'(0(2(3(z0)))), 0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(2(2(1(0(5(z0)))))), 0'(5(z0)), 5'(z0))
0'(1(5(2(z0)))) → c19(5'(5(0(2(1(3(z0)))))), 5'(0(2(1(3(z0))))), 0'(2(1(3(z0)))))
0'(2(4(2(z0)))) → c20(0'(5(4(3(2(2(z0)))))), 5'(4(3(2(2(z0))))))
0'(3(1(2(z0)))) → c21(0'(2(1(3(2(z0))))))
0'(3(1(2(z0)))) → c22(0'(2(5(3(z0)))), 5'(3(z0)))
0'(3(1(2(z0)))) → c23(5'(0(2(3(z0)))), 0'(2(3(z0))))
0'(3(1(2(z0)))) → c24(0'(2(2(1(z0)))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(3(1(2(z0)))) → c26(0'(3(2(3(1(3(z0)))))))
0'(3(4(2(z0)))) → c27(0'(2(2(3(4(z0))))))
0'(1(1(2(5(z0))))) → c28(5'(0(2(5(1(1(z0)))))), 0'(2(5(1(1(z0))))), 5'(1(1(z0))))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(3(1(2(5(z0))))) → c30(0'(5(z0)), 5'(z0))
0'(3(1(5(2(z0))))) → c31(0'(3(2(5(1(2(z0)))))), 5'(1(2(z0))))
0'(3(4(1(4(z0))))) → c32(0'(5(3(1(4(4(z0)))))), 5'(3(1(4(4(z0))))))
0'(3(5(1(2(z0))))) → c33(5'(5(3(2(1(0(z0)))))), 5'(3(2(1(0(z0))))), 0'(z0))
0'(4(0(4(2(z0))))) → c34(0'(0(2(2(z0)))), 0'(2(2(z0))))
0'(4(1(1(2(z0))))) → c35(0'(2(1(z0))))
0'(4(1(2(2(z0))))) → c36(0'(2(2(3(z0)))))
0'(4(1(2(5(z0))))) → c37(0'(2(5(z0))), 5'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(4(2(1(4(z0))))) → c39(0'(2(1(4(4(4(z0)))))))
0'(4(2(5(2(z0))))) → c40(5'(4(3(2(2(0(z0)))))), 0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))), 5'(5(z0)), 5'(z0))
0'(4(5(1(2(z0))))) → c42(0'(2(5(1(1(z0))))), 5'(1(1(z0))))
5'(0(1(2(z0)))) → c43(5'(0(z0)), 0'(z0))
5'(0(1(2(z0)))) → c44(5'(0(2(1(3(3(z0)))))), 0'(2(1(3(3(z0))))))
5'(0(1(2(2(z0))))) → c45(5'(0(2(2(1(2(z0)))))), 0'(2(2(1(2(z0))))))
5'(0(2(4(2(z0))))) → c46(0'(2(2(5(1(4(z0)))))), 5'(1(4(z0))))
5'(0(4(4(2(z0))))) → c47(0'(5(2(5(4(4(z0)))))), 5'(2(5(4(4(z0))))), 5'(4(4(z0))))
K tuples:none
Defined Rule Symbols:
0, 5
Defined Pair Symbols:
0', 5'
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47
(3) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
0'(0(4(2(z0)))) → c9(0'(0(2(2(3(4(z0)))))), 0'(2(2(3(4(z0))))))
0'(4(0(4(2(z0))))) → c34(0'(0(2(2(z0)))), 0'(2(2(z0))))
5'(0(1(2(z0)))) → c43(5'(0(z0)), 0'(z0))
5'(0(1(2(z0)))) → c44(5'(0(2(1(3(3(z0)))))), 0'(2(1(3(3(z0))))))
5'(0(1(2(2(z0))))) → c45(5'(0(2(2(1(2(z0)))))), 0'(2(2(1(2(z0))))))
5'(0(2(4(2(z0))))) → c46(0'(2(2(5(1(4(z0)))))), 5'(1(4(z0))))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(1(3(2(z0))))
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(2(2(1(z0))))
0(1(2(z0))) → 0(2(2(1(4(z0)))))
0(1(2(z0))) → 5(1(0(5(2(3(z0))))))
0(2(4(z0))) → 0(2(1(4(3(z0)))))
0(4(2(z0))) → 4(0(2(3(z0))))
0(4(2(z0))) → 4(0(5(5(2(z0)))))
0(0(4(2(z0)))) → 0(0(2(2(3(4(z0))))))
0(1(2(2(z0)))) → 0(2(1(0(2(z0)))))
0(1(2(2(z0)))) → 1(3(0(2(2(z0)))))
0(1(2(4(z0)))) → 0(1(4(2(3(z0)))))
0(1(2(4(z0)))) → 4(0(2(2(1(1(z0))))))
0(1(2(4(z0)))) → 4(0(5(5(2(1(z0))))))
0(1(2(5(z0)))) → 3(5(5(2(1(0(z0))))))
0(1(4(2(z0)))) → 0(5(2(1(4(z0)))))
0(1(5(2(z0)))) → 1(5(0(2(3(z0)))))
0(1(5(2(z0)))) → 0(2(2(1(0(5(z0))))))
0(1(5(2(z0)))) → 5(5(0(2(1(3(z0))))))
0(2(4(2(z0)))) → 0(5(4(3(2(2(z0))))))
0(3(1(2(z0)))) → 0(2(1(3(2(z0)))))
0(3(1(2(z0)))) → 1(0(2(5(3(z0)))))
0(3(1(2(z0)))) → 1(5(0(2(3(z0)))))
0(3(1(2(z0)))) → 3(0(2(2(1(z0)))))
0(3(1(2(z0)))) → 3(2(2(1(0(z0)))))
0(3(1(2(z0)))) → 0(3(2(3(1(3(z0))))))
0(3(4(2(z0)))) → 0(2(2(3(4(z0)))))
0(1(1(2(5(z0))))) → 5(0(2(5(1(1(z0))))))
0(2(3(4(2(z0))))) → 3(2(2(3(4(0(z0))))))
0(3(1(2(5(z0))))) → 2(3(1(3(0(5(z0))))))
0(3(1(5(2(z0))))) → 0(3(2(5(1(2(z0))))))
0(3(4(1(4(z0))))) → 0(5(3(1(4(4(z0))))))
0(3(5(1(2(z0))))) → 5(5(3(2(1(0(z0))))))
0(4(0(4(2(z0))))) → 4(4(0(0(2(2(z0))))))
0(4(1(1(2(z0))))) → 3(1(4(0(2(1(z0))))))
0(4(1(2(2(z0))))) → 4(1(0(2(2(3(z0))))))
0(4(1(2(5(z0))))) → 3(4(1(0(2(5(z0))))))
0(4(2(1(2(z0))))) → 4(1(3(2(0(2(z0))))))
0(4(2(1(4(z0))))) → 0(2(1(4(4(4(z0))))))
0(4(2(5(2(z0))))) → 5(4(3(2(2(0(z0))))))
0(4(5(1(2(z0))))) → 1(4(2(0(5(5(z0))))))
0(4(5(1(2(z0))))) → 4(0(2(5(1(1(z0))))))
5(0(1(2(z0)))) → 1(3(2(5(0(z0)))))
5(0(1(2(z0)))) → 5(0(2(1(3(3(z0))))))
5(0(1(2(2(z0))))) → 5(0(2(2(1(2(z0))))))
5(0(2(4(2(z0))))) → 0(2(2(5(1(4(z0))))))
5(0(4(4(2(z0))))) → 0(5(2(5(4(4(z0))))))
Tuples:
0'(1(2(z0))) → c(0'(1(3(2(z0)))))
0'(1(2(z0))) → c1(0'(2(1(0(z0)))), 0'(z0))
0'(1(2(z0))) → c2(0'(2(1(3(z0)))))
0'(1(2(z0))) → c3(0'(2(2(1(z0)))))
0'(1(2(z0))) → c4(0'(2(2(1(4(z0))))))
0'(1(2(z0))) → c5(5'(1(0(5(2(3(z0)))))), 0'(5(2(3(z0)))), 5'(2(3(z0))))
0'(2(4(z0))) → c6(0'(2(1(4(3(z0))))))
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(4(2(z0))) → c8(0'(5(5(2(z0)))), 5'(5(2(z0))), 5'(2(z0)))
0'(1(2(2(z0)))) → c10(0'(2(1(0(2(z0))))), 0'(2(z0)))
0'(1(2(2(z0)))) → c11(0'(2(2(z0))))
0'(1(2(4(z0)))) → c12(0'(1(4(2(3(z0))))))
0'(1(2(4(z0)))) → c13(0'(2(2(1(1(z0))))))
0'(1(2(4(z0)))) → c14(0'(5(5(2(1(z0))))), 5'(5(2(1(z0)))), 5'(2(1(z0))))
0'(1(4(2(z0)))) → c16(0'(5(2(1(4(z0))))), 5'(2(1(4(z0)))))
0'(2(4(2(z0)))) → c20(0'(5(4(3(2(2(z0)))))), 5'(4(3(2(2(z0))))))
0'(3(1(2(z0)))) → c21(0'(2(1(3(2(z0))))))
0'(3(1(2(z0)))) → c22(0'(2(5(3(z0)))), 5'(3(z0)))
0'(3(1(2(z0)))) → c23(5'(0(2(3(z0)))), 0'(2(3(z0))))
0'(3(1(2(z0)))) → c24(0'(2(2(1(z0)))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(3(1(2(z0)))) → c26(0'(3(2(3(1(3(z0)))))))
0'(3(4(2(z0)))) → c27(0'(2(2(3(4(z0))))))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(3(4(1(4(z0))))) → c32(0'(5(3(1(4(4(z0)))))), 5'(3(1(4(4(z0))))))
0'(4(1(1(2(z0))))) → c35(0'(2(1(z0))))
0'(4(1(2(2(z0))))) → c36(0'(2(2(3(z0)))))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(4(2(1(4(z0))))) → c39(0'(2(1(4(4(4(z0)))))))
0'(1(2(5(z0)))) → c15(5'(5(2(1(0(z0))))), 5'(2(1(0(z0)))), 0'(z0))
0'(1(5(2(z0)))) → c17(5'(0(2(3(z0)))), 0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(2(2(1(0(5(z0)))))), 0'(5(z0)), 5'(z0))
0'(1(5(2(z0)))) → c19(5'(5(0(2(1(3(z0)))))), 5'(0(2(1(3(z0))))), 0'(2(1(3(z0)))))
0'(1(1(2(5(z0))))) → c28(5'(0(2(5(1(1(z0)))))), 0'(2(5(1(1(z0))))), 5'(1(1(z0))))
0'(3(1(2(5(z0))))) → c30(0'(5(z0)), 5'(z0))
0'(3(1(5(2(z0))))) → c31(0'(3(2(5(1(2(z0)))))), 5'(1(2(z0))))
0'(3(5(1(2(z0))))) → c33(5'(5(3(2(1(0(z0)))))), 5'(3(2(1(0(z0))))), 0'(z0))
0'(4(1(2(5(z0))))) → c37(0'(2(5(z0))), 5'(z0))
0'(4(2(5(2(z0))))) → c40(5'(4(3(2(2(0(z0)))))), 0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))), 5'(5(z0)), 5'(z0))
0'(4(5(1(2(z0))))) → c42(0'(2(5(1(1(z0))))), 5'(1(1(z0))))
5'(0(4(4(2(z0))))) → c47(0'(5(2(5(4(4(z0)))))), 5'(2(5(4(4(z0))))), 5'(4(4(z0))))
S tuples:
0'(1(2(z0))) → c(0'(1(3(2(z0)))))
0'(1(2(z0))) → c1(0'(2(1(0(z0)))), 0'(z0))
0'(1(2(z0))) → c2(0'(2(1(3(z0)))))
0'(1(2(z0))) → c3(0'(2(2(1(z0)))))
0'(1(2(z0))) → c4(0'(2(2(1(4(z0))))))
0'(1(2(z0))) → c5(5'(1(0(5(2(3(z0)))))), 0'(5(2(3(z0)))), 5'(2(3(z0))))
0'(2(4(z0))) → c6(0'(2(1(4(3(z0))))))
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(4(2(z0))) → c8(0'(5(5(2(z0)))), 5'(5(2(z0))), 5'(2(z0)))
0'(1(2(2(z0)))) → c10(0'(2(1(0(2(z0))))), 0'(2(z0)))
0'(1(2(2(z0)))) → c11(0'(2(2(z0))))
0'(1(2(4(z0)))) → c12(0'(1(4(2(3(z0))))))
0'(1(2(4(z0)))) → c13(0'(2(2(1(1(z0))))))
0'(1(2(4(z0)))) → c14(0'(5(5(2(1(z0))))), 5'(5(2(1(z0)))), 5'(2(1(z0))))
0'(1(2(5(z0)))) → c15(5'(5(2(1(0(z0))))), 5'(2(1(0(z0)))), 0'(z0))
0'(1(4(2(z0)))) → c16(0'(5(2(1(4(z0))))), 5'(2(1(4(z0)))))
0'(1(5(2(z0)))) → c17(5'(0(2(3(z0)))), 0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(2(2(1(0(5(z0)))))), 0'(5(z0)), 5'(z0))
0'(1(5(2(z0)))) → c19(5'(5(0(2(1(3(z0)))))), 5'(0(2(1(3(z0))))), 0'(2(1(3(z0)))))
0'(2(4(2(z0)))) → c20(0'(5(4(3(2(2(z0)))))), 5'(4(3(2(2(z0))))))
0'(3(1(2(z0)))) → c21(0'(2(1(3(2(z0))))))
0'(3(1(2(z0)))) → c22(0'(2(5(3(z0)))), 5'(3(z0)))
0'(3(1(2(z0)))) → c23(5'(0(2(3(z0)))), 0'(2(3(z0))))
0'(3(1(2(z0)))) → c24(0'(2(2(1(z0)))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(3(1(2(z0)))) → c26(0'(3(2(3(1(3(z0)))))))
0'(3(4(2(z0)))) → c27(0'(2(2(3(4(z0))))))
0'(1(1(2(5(z0))))) → c28(5'(0(2(5(1(1(z0)))))), 0'(2(5(1(1(z0))))), 5'(1(1(z0))))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(3(1(2(5(z0))))) → c30(0'(5(z0)), 5'(z0))
0'(3(1(5(2(z0))))) → c31(0'(3(2(5(1(2(z0)))))), 5'(1(2(z0))))
0'(3(4(1(4(z0))))) → c32(0'(5(3(1(4(4(z0)))))), 5'(3(1(4(4(z0))))))
0'(3(5(1(2(z0))))) → c33(5'(5(3(2(1(0(z0)))))), 5'(3(2(1(0(z0))))), 0'(z0))
0'(4(1(1(2(z0))))) → c35(0'(2(1(z0))))
0'(4(1(2(2(z0))))) → c36(0'(2(2(3(z0)))))
0'(4(1(2(5(z0))))) → c37(0'(2(5(z0))), 5'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(4(2(1(4(z0))))) → c39(0'(2(1(4(4(4(z0)))))))
0'(4(2(5(2(z0))))) → c40(5'(4(3(2(2(0(z0)))))), 0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))), 5'(5(z0)), 5'(z0))
0'(4(5(1(2(z0))))) → c42(0'(2(5(1(1(z0))))), 5'(1(1(z0))))
5'(0(4(4(2(z0))))) → c47(0'(5(2(5(4(4(z0)))))), 5'(2(5(4(4(z0))))), 5'(4(4(z0))))
K tuples:none
Defined Rule Symbols:
0, 5
Defined Pair Symbols:
0', 5'
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7, c8, c10, c11, c12, c13, c14, c16, c20, c21, c22, c23, c24, c25, c26, c27, c29, c32, c35, c36, c38, c39, c15, c17, c18, c19, c28, c30, c31, c33, c37, c40, c41, c42, c47
(5) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)
Removed 29 of 42 dangling nodes:
0'(1(2(z0))) → c(0'(1(3(2(z0)))))
0'(1(2(z0))) → c2(0'(2(1(3(z0)))))
0'(1(2(z0))) → c3(0'(2(2(1(z0)))))
0'(1(2(z0))) → c4(0'(2(2(1(4(z0))))))
0'(1(2(z0))) → c5(5'(1(0(5(2(3(z0)))))), 0'(5(2(3(z0)))), 5'(2(3(z0))))
0'(2(4(z0))) → c6(0'(2(1(4(3(z0))))))
0'(4(2(z0))) → c8(0'(5(5(2(z0)))), 5'(5(2(z0))), 5'(2(z0)))
0'(1(2(2(z0)))) → c11(0'(2(2(z0))))
0'(1(2(4(z0)))) → c12(0'(1(4(2(3(z0))))))
0'(1(2(4(z0)))) → c13(0'(2(2(1(1(z0))))))
0'(1(2(4(z0)))) → c14(0'(5(5(2(1(z0))))), 5'(5(2(1(z0)))), 5'(2(1(z0))))
0'(1(4(2(z0)))) → c16(0'(5(2(1(4(z0))))), 5'(2(1(4(z0)))))
0'(2(4(2(z0)))) → c20(0'(5(4(3(2(2(z0)))))), 5'(4(3(2(2(z0))))))
0'(1(5(2(z0)))) → c19(5'(5(0(2(1(3(z0)))))), 5'(0(2(1(3(z0))))), 0'(2(1(3(z0)))))
0'(3(1(2(z0)))) → c22(0'(2(5(3(z0)))), 5'(3(z0)))
0'(3(1(2(z0)))) → c21(0'(2(1(3(2(z0))))))
0'(3(1(2(z0)))) → c24(0'(2(2(1(z0)))))
0'(3(1(2(z0)))) → c26(0'(3(2(3(1(3(z0)))))))
0'(1(1(2(5(z0))))) → c28(5'(0(2(5(1(1(z0)))))), 0'(2(5(1(1(z0))))), 5'(1(1(z0))))
0'(3(4(2(z0)))) → c27(0'(2(2(3(4(z0))))))
0'(3(1(2(5(z0))))) → c30(0'(5(z0)), 5'(z0))
0'(3(1(5(2(z0))))) → c31(0'(3(2(5(1(2(z0)))))), 5'(1(2(z0))))
0'(3(4(1(4(z0))))) → c32(0'(5(3(1(4(4(z0)))))), 5'(3(1(4(4(z0))))))
0'(4(1(2(5(z0))))) → c37(0'(2(5(z0))), 5'(z0))
0'(4(1(1(2(z0))))) → c35(0'(2(1(z0))))
0'(4(1(2(2(z0))))) → c36(0'(2(2(3(z0)))))
0'(4(5(1(2(z0))))) → c42(0'(2(5(1(1(z0))))), 5'(1(1(z0))))
0'(4(2(1(4(z0))))) → c39(0'(2(1(4(4(4(z0)))))))
5'(0(4(4(2(z0))))) → c47(0'(5(2(5(4(4(z0)))))), 5'(2(5(4(4(z0))))), 5'(4(4(z0))))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(1(3(2(z0))))
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(2(2(1(z0))))
0(1(2(z0))) → 0(2(2(1(4(z0)))))
0(1(2(z0))) → 5(1(0(5(2(3(z0))))))
0(2(4(z0))) → 0(2(1(4(3(z0)))))
0(4(2(z0))) → 4(0(2(3(z0))))
0(4(2(z0))) → 4(0(5(5(2(z0)))))
0(0(4(2(z0)))) → 0(0(2(2(3(4(z0))))))
0(1(2(2(z0)))) → 0(2(1(0(2(z0)))))
0(1(2(2(z0)))) → 1(3(0(2(2(z0)))))
0(1(2(4(z0)))) → 0(1(4(2(3(z0)))))
0(1(2(4(z0)))) → 4(0(2(2(1(1(z0))))))
0(1(2(4(z0)))) → 4(0(5(5(2(1(z0))))))
0(1(2(5(z0)))) → 3(5(5(2(1(0(z0))))))
0(1(4(2(z0)))) → 0(5(2(1(4(z0)))))
0(1(5(2(z0)))) → 1(5(0(2(3(z0)))))
0(1(5(2(z0)))) → 0(2(2(1(0(5(z0))))))
0(1(5(2(z0)))) → 5(5(0(2(1(3(z0))))))
0(2(4(2(z0)))) → 0(5(4(3(2(2(z0))))))
0(3(1(2(z0)))) → 0(2(1(3(2(z0)))))
0(3(1(2(z0)))) → 1(0(2(5(3(z0)))))
0(3(1(2(z0)))) → 1(5(0(2(3(z0)))))
0(3(1(2(z0)))) → 3(0(2(2(1(z0)))))
0(3(1(2(z0)))) → 3(2(2(1(0(z0)))))
0(3(1(2(z0)))) → 0(3(2(3(1(3(z0))))))
0(3(4(2(z0)))) → 0(2(2(3(4(z0)))))
0(1(1(2(5(z0))))) → 5(0(2(5(1(1(z0))))))
0(2(3(4(2(z0))))) → 3(2(2(3(4(0(z0))))))
0(3(1(2(5(z0))))) → 2(3(1(3(0(5(z0))))))
0(3(1(5(2(z0))))) → 0(3(2(5(1(2(z0))))))
0(3(4(1(4(z0))))) → 0(5(3(1(4(4(z0))))))
0(3(5(1(2(z0))))) → 5(5(3(2(1(0(z0))))))
0(4(0(4(2(z0))))) → 4(4(0(0(2(2(z0))))))
0(4(1(1(2(z0))))) → 3(1(4(0(2(1(z0))))))
0(4(1(2(2(z0))))) → 4(1(0(2(2(3(z0))))))
0(4(1(2(5(z0))))) → 3(4(1(0(2(5(z0))))))
0(4(2(1(2(z0))))) → 4(1(3(2(0(2(z0))))))
0(4(2(1(4(z0))))) → 0(2(1(4(4(4(z0))))))
0(4(2(5(2(z0))))) → 5(4(3(2(2(0(z0))))))
0(4(5(1(2(z0))))) → 1(4(2(0(5(5(z0))))))
0(4(5(1(2(z0))))) → 4(0(2(5(1(1(z0))))))
5(0(1(2(z0)))) → 1(3(2(5(0(z0)))))
5(0(1(2(z0)))) → 5(0(2(1(3(3(z0))))))
5(0(1(2(2(z0))))) → 5(0(2(2(1(2(z0))))))
5(0(2(4(2(z0))))) → 0(2(2(5(1(4(z0))))))
5(0(4(4(2(z0))))) → 0(5(2(5(4(4(z0))))))
Tuples:
0'(1(2(z0))) → c1(0'(2(1(0(z0)))), 0'(z0))
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(1(2(2(z0)))) → c10(0'(2(1(0(2(z0))))), 0'(2(z0)))
0'(3(1(2(z0)))) → c23(5'(0(2(3(z0)))), 0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(1(2(5(z0)))) → c15(5'(5(2(1(0(z0))))), 5'(2(1(0(z0)))), 0'(z0))
0'(1(5(2(z0)))) → c17(5'(0(2(3(z0)))), 0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(2(2(1(0(5(z0)))))), 0'(5(z0)), 5'(z0))
0'(3(5(1(2(z0))))) → c33(5'(5(3(2(1(0(z0)))))), 5'(3(2(1(0(z0))))), 0'(z0))
0'(4(2(5(2(z0))))) → c40(5'(4(3(2(2(0(z0)))))), 0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))), 5'(5(z0)), 5'(z0))
S tuples:
0'(1(2(z0))) → c1(0'(2(1(0(z0)))), 0'(z0))
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(1(2(2(z0)))) → c10(0'(2(1(0(2(z0))))), 0'(2(z0)))
0'(1(2(5(z0)))) → c15(5'(5(2(1(0(z0))))), 5'(2(1(0(z0)))), 0'(z0))
0'(1(5(2(z0)))) → c17(5'(0(2(3(z0)))), 0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(2(2(1(0(5(z0)))))), 0'(5(z0)), 5'(z0))
0'(3(1(2(z0)))) → c23(5'(0(2(3(z0)))), 0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(3(5(1(2(z0))))) → c33(5'(5(3(2(1(0(z0)))))), 5'(3(2(1(0(z0))))), 0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(4(2(5(2(z0))))) → c40(5'(4(3(2(2(0(z0)))))), 0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))), 5'(5(z0)), 5'(z0))
K tuples:none
Defined Rule Symbols:
0, 5
Defined Pair Symbols:
0'
Compound Symbols:
c1, c7, c10, c23, c25, c29, c38, c15, c17, c18, c33, c40, c41
(7) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)
Removed 13 trailing tuple parts
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(1(3(2(z0))))
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(2(2(1(z0))))
0(1(2(z0))) → 0(2(2(1(4(z0)))))
0(1(2(z0))) → 5(1(0(5(2(3(z0))))))
0(2(4(z0))) → 0(2(1(4(3(z0)))))
0(4(2(z0))) → 4(0(2(3(z0))))
0(4(2(z0))) → 4(0(5(5(2(z0)))))
0(0(4(2(z0)))) → 0(0(2(2(3(4(z0))))))
0(1(2(2(z0)))) → 0(2(1(0(2(z0)))))
0(1(2(2(z0)))) → 1(3(0(2(2(z0)))))
0(1(2(4(z0)))) → 0(1(4(2(3(z0)))))
0(1(2(4(z0)))) → 4(0(2(2(1(1(z0))))))
0(1(2(4(z0)))) → 4(0(5(5(2(1(z0))))))
0(1(2(5(z0)))) → 3(5(5(2(1(0(z0))))))
0(1(4(2(z0)))) → 0(5(2(1(4(z0)))))
0(1(5(2(z0)))) → 1(5(0(2(3(z0)))))
0(1(5(2(z0)))) → 0(2(2(1(0(5(z0))))))
0(1(5(2(z0)))) → 5(5(0(2(1(3(z0))))))
0(2(4(2(z0)))) → 0(5(4(3(2(2(z0))))))
0(3(1(2(z0)))) → 0(2(1(3(2(z0)))))
0(3(1(2(z0)))) → 1(0(2(5(3(z0)))))
0(3(1(2(z0)))) → 1(5(0(2(3(z0)))))
0(3(1(2(z0)))) → 3(0(2(2(1(z0)))))
0(3(1(2(z0)))) → 3(2(2(1(0(z0)))))
0(3(1(2(z0)))) → 0(3(2(3(1(3(z0))))))
0(3(4(2(z0)))) → 0(2(2(3(4(z0)))))
0(1(1(2(5(z0))))) → 5(0(2(5(1(1(z0))))))
0(2(3(4(2(z0))))) → 3(2(2(3(4(0(z0))))))
0(3(1(2(5(z0))))) → 2(3(1(3(0(5(z0))))))
0(3(1(5(2(z0))))) → 0(3(2(5(1(2(z0))))))
0(3(4(1(4(z0))))) → 0(5(3(1(4(4(z0))))))
0(3(5(1(2(z0))))) → 5(5(3(2(1(0(z0))))))
0(4(0(4(2(z0))))) → 4(4(0(0(2(2(z0))))))
0(4(1(1(2(z0))))) → 3(1(4(0(2(1(z0))))))
0(4(1(2(2(z0))))) → 4(1(0(2(2(3(z0))))))
0(4(1(2(5(z0))))) → 3(4(1(0(2(5(z0))))))
0(4(2(1(2(z0))))) → 4(1(3(2(0(2(z0))))))
0(4(2(1(4(z0))))) → 0(2(1(4(4(4(z0))))))
0(4(2(5(2(z0))))) → 5(4(3(2(2(0(z0))))))
0(4(5(1(2(z0))))) → 1(4(2(0(5(5(z0))))))
0(4(5(1(2(z0))))) → 4(0(2(5(1(1(z0))))))
5(0(1(2(z0)))) → 1(3(2(5(0(z0)))))
5(0(1(2(z0)))) → 5(0(2(1(3(3(z0))))))
5(0(1(2(2(z0))))) → 5(0(2(2(1(2(z0))))))
5(0(2(4(2(z0))))) → 0(2(2(5(1(4(z0))))))
5(0(4(4(2(z0))))) → 0(5(2(5(4(4(z0))))))
Tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(1(2(z0))) → c1(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
S tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(1(2(z0))) → c1(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
K tuples:none
Defined Rule Symbols:
0, 5
Defined Pair Symbols:
0'
Compound Symbols:
c7, c25, c29, c38, c1, c10, c23, c15, c17, c18, c33, c40, c41
(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
0'(1(2(z0))) → c1(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
We considered the (Usable) Rules:
5(0(4(4(2(z0))))) → 0(5(2(5(4(4(z0))))))
And the Tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(1(2(z0))) → c1(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0(x1)) = [4]
POL(0'(x1)) = [2]x1
POL(1(x1)) = [2] + x1
POL(2(x1)) = x1
POL(3(x1)) = [4] + x1
POL(4(x1)) = [4] + x1
POL(5(x1)) = [2] + x1
POL(c1(x1)) = x1
POL(c10(x1)) = x1
POL(c15(x1)) = x1
POL(c17(x1)) = x1
POL(c18(x1)) = x1
POL(c23(x1)) = x1
POL(c25(x1)) = x1
POL(c29(x1)) = x1
POL(c33(x1)) = x1
POL(c38(x1)) = x1
POL(c40(x1)) = x1
POL(c41(x1)) = x1
POL(c7(x1)) = x1
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(1(3(2(z0))))
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(2(2(1(z0))))
0(1(2(z0))) → 0(2(2(1(4(z0)))))
0(1(2(z0))) → 5(1(0(5(2(3(z0))))))
0(2(4(z0))) → 0(2(1(4(3(z0)))))
0(4(2(z0))) → 4(0(2(3(z0))))
0(4(2(z0))) → 4(0(5(5(2(z0)))))
0(0(4(2(z0)))) → 0(0(2(2(3(4(z0))))))
0(1(2(2(z0)))) → 0(2(1(0(2(z0)))))
0(1(2(2(z0)))) → 1(3(0(2(2(z0)))))
0(1(2(4(z0)))) → 0(1(4(2(3(z0)))))
0(1(2(4(z0)))) → 4(0(2(2(1(1(z0))))))
0(1(2(4(z0)))) → 4(0(5(5(2(1(z0))))))
0(1(2(5(z0)))) → 3(5(5(2(1(0(z0))))))
0(1(4(2(z0)))) → 0(5(2(1(4(z0)))))
0(1(5(2(z0)))) → 1(5(0(2(3(z0)))))
0(1(5(2(z0)))) → 0(2(2(1(0(5(z0))))))
0(1(5(2(z0)))) → 5(5(0(2(1(3(z0))))))
0(2(4(2(z0)))) → 0(5(4(3(2(2(z0))))))
0(3(1(2(z0)))) → 0(2(1(3(2(z0)))))
0(3(1(2(z0)))) → 1(0(2(5(3(z0)))))
0(3(1(2(z0)))) → 1(5(0(2(3(z0)))))
0(3(1(2(z0)))) → 3(0(2(2(1(z0)))))
0(3(1(2(z0)))) → 3(2(2(1(0(z0)))))
0(3(1(2(z0)))) → 0(3(2(3(1(3(z0))))))
0(3(4(2(z0)))) → 0(2(2(3(4(z0)))))
0(1(1(2(5(z0))))) → 5(0(2(5(1(1(z0))))))
0(2(3(4(2(z0))))) → 3(2(2(3(4(0(z0))))))
0(3(1(2(5(z0))))) → 2(3(1(3(0(5(z0))))))
0(3(1(5(2(z0))))) → 0(3(2(5(1(2(z0))))))
0(3(4(1(4(z0))))) → 0(5(3(1(4(4(z0))))))
0(3(5(1(2(z0))))) → 5(5(3(2(1(0(z0))))))
0(4(0(4(2(z0))))) → 4(4(0(0(2(2(z0))))))
0(4(1(1(2(z0))))) → 3(1(4(0(2(1(z0))))))
0(4(1(2(2(z0))))) → 4(1(0(2(2(3(z0))))))
0(4(1(2(5(z0))))) → 3(4(1(0(2(5(z0))))))
0(4(2(1(2(z0))))) → 4(1(3(2(0(2(z0))))))
0(4(2(1(4(z0))))) → 0(2(1(4(4(4(z0))))))
0(4(2(5(2(z0))))) → 5(4(3(2(2(0(z0))))))
0(4(5(1(2(z0))))) → 1(4(2(0(5(5(z0))))))
0(4(5(1(2(z0))))) → 4(0(2(5(1(1(z0))))))
5(0(1(2(z0)))) → 1(3(2(5(0(z0)))))
5(0(1(2(z0)))) → 5(0(2(1(3(3(z0))))))
5(0(1(2(2(z0))))) → 5(0(2(2(1(2(z0))))))
5(0(2(4(2(z0))))) → 0(2(2(5(1(4(z0))))))
5(0(4(4(2(z0))))) → 0(5(2(5(4(4(z0))))))
Tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(1(2(z0))) → c1(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
S tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
K tuples:
0'(1(2(z0))) → c1(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
Defined Rule Symbols:
0, 5
Defined Pair Symbols:
0'
Compound Symbols:
c7, c25, c29, c38, c1, c10, c23, c15, c17, c18, c33, c40, c41
(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
We considered the (Usable) Rules:
5(0(4(4(2(z0))))) → 0(5(2(5(4(4(z0))))))
And the Tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(1(2(z0))) → c1(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0(x1)) = [4]
POL(0'(x1)) = [4]x1
POL(1(x1)) = x1
POL(2(x1)) = x1
POL(3(x1)) = x1
POL(4(x1)) = [2] + x1
POL(5(x1)) = x1
POL(c1(x1)) = x1
POL(c10(x1)) = x1
POL(c15(x1)) = x1
POL(c17(x1)) = x1
POL(c18(x1)) = x1
POL(c23(x1)) = x1
POL(c25(x1)) = x1
POL(c29(x1)) = x1
POL(c33(x1)) = x1
POL(c38(x1)) = x1
POL(c40(x1)) = x1
POL(c41(x1)) = x1
POL(c7(x1)) = x1
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(1(3(2(z0))))
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(2(2(1(z0))))
0(1(2(z0))) → 0(2(2(1(4(z0)))))
0(1(2(z0))) → 5(1(0(5(2(3(z0))))))
0(2(4(z0))) → 0(2(1(4(3(z0)))))
0(4(2(z0))) → 4(0(2(3(z0))))
0(4(2(z0))) → 4(0(5(5(2(z0)))))
0(0(4(2(z0)))) → 0(0(2(2(3(4(z0))))))
0(1(2(2(z0)))) → 0(2(1(0(2(z0)))))
0(1(2(2(z0)))) → 1(3(0(2(2(z0)))))
0(1(2(4(z0)))) → 0(1(4(2(3(z0)))))
0(1(2(4(z0)))) → 4(0(2(2(1(1(z0))))))
0(1(2(4(z0)))) → 4(0(5(5(2(1(z0))))))
0(1(2(5(z0)))) → 3(5(5(2(1(0(z0))))))
0(1(4(2(z0)))) → 0(5(2(1(4(z0)))))
0(1(5(2(z0)))) → 1(5(0(2(3(z0)))))
0(1(5(2(z0)))) → 0(2(2(1(0(5(z0))))))
0(1(5(2(z0)))) → 5(5(0(2(1(3(z0))))))
0(2(4(2(z0)))) → 0(5(4(3(2(2(z0))))))
0(3(1(2(z0)))) → 0(2(1(3(2(z0)))))
0(3(1(2(z0)))) → 1(0(2(5(3(z0)))))
0(3(1(2(z0)))) → 1(5(0(2(3(z0)))))
0(3(1(2(z0)))) → 3(0(2(2(1(z0)))))
0(3(1(2(z0)))) → 3(2(2(1(0(z0)))))
0(3(1(2(z0)))) → 0(3(2(3(1(3(z0))))))
0(3(4(2(z0)))) → 0(2(2(3(4(z0)))))
0(1(1(2(5(z0))))) → 5(0(2(5(1(1(z0))))))
0(2(3(4(2(z0))))) → 3(2(2(3(4(0(z0))))))
0(3(1(2(5(z0))))) → 2(3(1(3(0(5(z0))))))
0(3(1(5(2(z0))))) → 0(3(2(5(1(2(z0))))))
0(3(4(1(4(z0))))) → 0(5(3(1(4(4(z0))))))
0(3(5(1(2(z0))))) → 5(5(3(2(1(0(z0))))))
0(4(0(4(2(z0))))) → 4(4(0(0(2(2(z0))))))
0(4(1(1(2(z0))))) → 3(1(4(0(2(1(z0))))))
0(4(1(2(2(z0))))) → 4(1(0(2(2(3(z0))))))
0(4(1(2(5(z0))))) → 3(4(1(0(2(5(z0))))))
0(4(2(1(2(z0))))) → 4(1(3(2(0(2(z0))))))
0(4(2(1(4(z0))))) → 0(2(1(4(4(4(z0))))))
0(4(2(5(2(z0))))) → 5(4(3(2(2(0(z0))))))
0(4(5(1(2(z0))))) → 1(4(2(0(5(5(z0))))))
0(4(5(1(2(z0))))) → 4(0(2(5(1(1(z0))))))
5(0(1(2(z0)))) → 1(3(2(5(0(z0)))))
5(0(1(2(z0)))) → 5(0(2(1(3(3(z0))))))
5(0(1(2(2(z0))))) → 5(0(2(2(1(2(z0))))))
5(0(2(4(2(z0))))) → 0(2(2(5(1(4(z0))))))
5(0(4(4(2(z0))))) → 0(5(2(5(4(4(z0))))))
Tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(1(2(z0))) → c1(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
S tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
K tuples:
0'(1(2(z0))) → c1(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
Defined Rule Symbols:
0, 5
Defined Pair Symbols:
0'
Compound Symbols:
c7, c25, c29, c38, c1, c10, c23, c15, c17, c18, c33, c40, c41
(13) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
We considered the (Usable) Rules:
5(0(4(4(2(z0))))) → 0(5(2(5(4(4(z0))))))
And the Tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(1(2(z0))) → c1(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0(x1)) = [4]
POL(0'(x1)) = [4]x1
POL(1(x1)) = [2] + x1
POL(2(x1)) = x1
POL(3(x1)) = [2] + x1
POL(4(x1)) = [2] + x1
POL(5(x1)) = x1
POL(c1(x1)) = x1
POL(c10(x1)) = x1
POL(c15(x1)) = x1
POL(c17(x1)) = x1
POL(c18(x1)) = x1
POL(c23(x1)) = x1
POL(c25(x1)) = x1
POL(c29(x1)) = x1
POL(c33(x1)) = x1
POL(c38(x1)) = x1
POL(c40(x1)) = x1
POL(c41(x1)) = x1
POL(c7(x1)) = x1
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(1(3(2(z0))))
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(2(2(1(z0))))
0(1(2(z0))) → 0(2(2(1(4(z0)))))
0(1(2(z0))) → 5(1(0(5(2(3(z0))))))
0(2(4(z0))) → 0(2(1(4(3(z0)))))
0(4(2(z0))) → 4(0(2(3(z0))))
0(4(2(z0))) → 4(0(5(5(2(z0)))))
0(0(4(2(z0)))) → 0(0(2(2(3(4(z0))))))
0(1(2(2(z0)))) → 0(2(1(0(2(z0)))))
0(1(2(2(z0)))) → 1(3(0(2(2(z0)))))
0(1(2(4(z0)))) → 0(1(4(2(3(z0)))))
0(1(2(4(z0)))) → 4(0(2(2(1(1(z0))))))
0(1(2(4(z0)))) → 4(0(5(5(2(1(z0))))))
0(1(2(5(z0)))) → 3(5(5(2(1(0(z0))))))
0(1(4(2(z0)))) → 0(5(2(1(4(z0)))))
0(1(5(2(z0)))) → 1(5(0(2(3(z0)))))
0(1(5(2(z0)))) → 0(2(2(1(0(5(z0))))))
0(1(5(2(z0)))) → 5(5(0(2(1(3(z0))))))
0(2(4(2(z0)))) → 0(5(4(3(2(2(z0))))))
0(3(1(2(z0)))) → 0(2(1(3(2(z0)))))
0(3(1(2(z0)))) → 1(0(2(5(3(z0)))))
0(3(1(2(z0)))) → 1(5(0(2(3(z0)))))
0(3(1(2(z0)))) → 3(0(2(2(1(z0)))))
0(3(1(2(z0)))) → 3(2(2(1(0(z0)))))
0(3(1(2(z0)))) → 0(3(2(3(1(3(z0))))))
0(3(4(2(z0)))) → 0(2(2(3(4(z0)))))
0(1(1(2(5(z0))))) → 5(0(2(5(1(1(z0))))))
0(2(3(4(2(z0))))) → 3(2(2(3(4(0(z0))))))
0(3(1(2(5(z0))))) → 2(3(1(3(0(5(z0))))))
0(3(1(5(2(z0))))) → 0(3(2(5(1(2(z0))))))
0(3(4(1(4(z0))))) → 0(5(3(1(4(4(z0))))))
0(3(5(1(2(z0))))) → 5(5(3(2(1(0(z0))))))
0(4(0(4(2(z0))))) → 4(4(0(0(2(2(z0))))))
0(4(1(1(2(z0))))) → 3(1(4(0(2(1(z0))))))
0(4(1(2(2(z0))))) → 4(1(0(2(2(3(z0))))))
0(4(1(2(5(z0))))) → 3(4(1(0(2(5(z0))))))
0(4(2(1(2(z0))))) → 4(1(3(2(0(2(z0))))))
0(4(2(1(4(z0))))) → 0(2(1(4(4(4(z0))))))
0(4(2(5(2(z0))))) → 5(4(3(2(2(0(z0))))))
0(4(5(1(2(z0))))) → 1(4(2(0(5(5(z0))))))
0(4(5(1(2(z0))))) → 4(0(2(5(1(1(z0))))))
5(0(1(2(z0)))) → 1(3(2(5(0(z0)))))
5(0(1(2(z0)))) → 5(0(2(1(3(3(z0))))))
5(0(1(2(2(z0))))) → 5(0(2(2(1(2(z0))))))
5(0(2(4(2(z0))))) → 0(2(2(5(1(4(z0))))))
5(0(4(4(2(z0))))) → 0(5(2(5(4(4(z0))))))
Tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(1(2(z0))) → c1(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
S tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
K tuples:
0'(1(2(z0))) → c1(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
Defined Rule Symbols:
0, 5
Defined Pair Symbols:
0'
Compound Symbols:
c7, c25, c29, c38, c1, c10, c23, c15, c17, c18, c33, c40, c41
(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(3(5(1(2(z0))))) → c33(0'(z0))
We considered the (Usable) Rules:
5(0(4(4(2(z0))))) → 0(5(2(5(4(4(z0))))))
And the Tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(1(2(z0))) → c1(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0(x1)) = [3]
POL(0'(x1)) = [4]x1
POL(1(x1)) = x1
POL(2(x1)) = x1
POL(3(x1)) = x1
POL(4(x1)) = [2] + x1
POL(5(x1)) = [1] + x1
POL(c1(x1)) = x1
POL(c10(x1)) = x1
POL(c15(x1)) = x1
POL(c17(x1)) = x1
POL(c18(x1)) = x1
POL(c23(x1)) = x1
POL(c25(x1)) = x1
POL(c29(x1)) = x1
POL(c33(x1)) = x1
POL(c38(x1)) = x1
POL(c40(x1)) = x1
POL(c41(x1)) = x1
POL(c7(x1)) = x1
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(1(3(2(z0))))
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(2(2(1(z0))))
0(1(2(z0))) → 0(2(2(1(4(z0)))))
0(1(2(z0))) → 5(1(0(5(2(3(z0))))))
0(2(4(z0))) → 0(2(1(4(3(z0)))))
0(4(2(z0))) → 4(0(2(3(z0))))
0(4(2(z0))) → 4(0(5(5(2(z0)))))
0(0(4(2(z0)))) → 0(0(2(2(3(4(z0))))))
0(1(2(2(z0)))) → 0(2(1(0(2(z0)))))
0(1(2(2(z0)))) → 1(3(0(2(2(z0)))))
0(1(2(4(z0)))) → 0(1(4(2(3(z0)))))
0(1(2(4(z0)))) → 4(0(2(2(1(1(z0))))))
0(1(2(4(z0)))) → 4(0(5(5(2(1(z0))))))
0(1(2(5(z0)))) → 3(5(5(2(1(0(z0))))))
0(1(4(2(z0)))) → 0(5(2(1(4(z0)))))
0(1(5(2(z0)))) → 1(5(0(2(3(z0)))))
0(1(5(2(z0)))) → 0(2(2(1(0(5(z0))))))
0(1(5(2(z0)))) → 5(5(0(2(1(3(z0))))))
0(2(4(2(z0)))) → 0(5(4(3(2(2(z0))))))
0(3(1(2(z0)))) → 0(2(1(3(2(z0)))))
0(3(1(2(z0)))) → 1(0(2(5(3(z0)))))
0(3(1(2(z0)))) → 1(5(0(2(3(z0)))))
0(3(1(2(z0)))) → 3(0(2(2(1(z0)))))
0(3(1(2(z0)))) → 3(2(2(1(0(z0)))))
0(3(1(2(z0)))) → 0(3(2(3(1(3(z0))))))
0(3(4(2(z0)))) → 0(2(2(3(4(z0)))))
0(1(1(2(5(z0))))) → 5(0(2(5(1(1(z0))))))
0(2(3(4(2(z0))))) → 3(2(2(3(4(0(z0))))))
0(3(1(2(5(z0))))) → 2(3(1(3(0(5(z0))))))
0(3(1(5(2(z0))))) → 0(3(2(5(1(2(z0))))))
0(3(4(1(4(z0))))) → 0(5(3(1(4(4(z0))))))
0(3(5(1(2(z0))))) → 5(5(3(2(1(0(z0))))))
0(4(0(4(2(z0))))) → 4(4(0(0(2(2(z0))))))
0(4(1(1(2(z0))))) → 3(1(4(0(2(1(z0))))))
0(4(1(2(2(z0))))) → 4(1(0(2(2(3(z0))))))
0(4(1(2(5(z0))))) → 3(4(1(0(2(5(z0))))))
0(4(2(1(2(z0))))) → 4(1(3(2(0(2(z0))))))
0(4(2(1(4(z0))))) → 0(2(1(4(4(4(z0))))))
0(4(2(5(2(z0))))) → 5(4(3(2(2(0(z0))))))
0(4(5(1(2(z0))))) → 1(4(2(0(5(5(z0))))))
0(4(5(1(2(z0))))) → 4(0(2(5(1(1(z0))))))
5(0(1(2(z0)))) → 1(3(2(5(0(z0)))))
5(0(1(2(z0)))) → 5(0(2(1(3(3(z0))))))
5(0(1(2(2(z0))))) → 5(0(2(2(1(2(z0))))))
5(0(2(4(2(z0))))) → 0(2(2(5(1(4(z0))))))
5(0(4(4(2(z0))))) → 0(5(2(5(4(4(z0))))))
Tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(1(2(z0))) → c1(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
S tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
K tuples:
0'(1(2(z0))) → c1(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(3(5(1(2(z0))))) → c33(0'(z0))
Defined Rule Symbols:
0, 5
Defined Pair Symbols:
0'
Compound Symbols:
c7, c25, c29, c38, c1, c10, c23, c15, c17, c18, c33, c40, c41
(17) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
0'(3(1(2(z0)))) → c25(0'(z0))
We considered the (Usable) Rules:
5(0(4(4(2(z0))))) → 0(5(2(5(4(4(z0))))))
And the Tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(1(2(z0))) → c1(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0(x1)) = [4]
POL(0'(x1)) = [4]x1
POL(1(x1)) = x1
POL(2(x1)) = x1
POL(3(x1)) = [3] + x1
POL(4(x1)) = [5] + x1
POL(5(x1)) = [4] + x1
POL(c1(x1)) = x1
POL(c10(x1)) = x1
POL(c15(x1)) = x1
POL(c17(x1)) = x1
POL(c18(x1)) = x1
POL(c23(x1)) = x1
POL(c25(x1)) = x1
POL(c29(x1)) = x1
POL(c33(x1)) = x1
POL(c38(x1)) = x1
POL(c40(x1)) = x1
POL(c41(x1)) = x1
POL(c7(x1)) = x1
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(1(3(2(z0))))
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(2(2(1(z0))))
0(1(2(z0))) → 0(2(2(1(4(z0)))))
0(1(2(z0))) → 5(1(0(5(2(3(z0))))))
0(2(4(z0))) → 0(2(1(4(3(z0)))))
0(4(2(z0))) → 4(0(2(3(z0))))
0(4(2(z0))) → 4(0(5(5(2(z0)))))
0(0(4(2(z0)))) → 0(0(2(2(3(4(z0))))))
0(1(2(2(z0)))) → 0(2(1(0(2(z0)))))
0(1(2(2(z0)))) → 1(3(0(2(2(z0)))))
0(1(2(4(z0)))) → 0(1(4(2(3(z0)))))
0(1(2(4(z0)))) → 4(0(2(2(1(1(z0))))))
0(1(2(4(z0)))) → 4(0(5(5(2(1(z0))))))
0(1(2(5(z0)))) → 3(5(5(2(1(0(z0))))))
0(1(4(2(z0)))) → 0(5(2(1(4(z0)))))
0(1(5(2(z0)))) → 1(5(0(2(3(z0)))))
0(1(5(2(z0)))) → 0(2(2(1(0(5(z0))))))
0(1(5(2(z0)))) → 5(5(0(2(1(3(z0))))))
0(2(4(2(z0)))) → 0(5(4(3(2(2(z0))))))
0(3(1(2(z0)))) → 0(2(1(3(2(z0)))))
0(3(1(2(z0)))) → 1(0(2(5(3(z0)))))
0(3(1(2(z0)))) → 1(5(0(2(3(z0)))))
0(3(1(2(z0)))) → 3(0(2(2(1(z0)))))
0(3(1(2(z0)))) → 3(2(2(1(0(z0)))))
0(3(1(2(z0)))) → 0(3(2(3(1(3(z0))))))
0(3(4(2(z0)))) → 0(2(2(3(4(z0)))))
0(1(1(2(5(z0))))) → 5(0(2(5(1(1(z0))))))
0(2(3(4(2(z0))))) → 3(2(2(3(4(0(z0))))))
0(3(1(2(5(z0))))) → 2(3(1(3(0(5(z0))))))
0(3(1(5(2(z0))))) → 0(3(2(5(1(2(z0))))))
0(3(4(1(4(z0))))) → 0(5(3(1(4(4(z0))))))
0(3(5(1(2(z0))))) → 5(5(3(2(1(0(z0))))))
0(4(0(4(2(z0))))) → 4(4(0(0(2(2(z0))))))
0(4(1(1(2(z0))))) → 3(1(4(0(2(1(z0))))))
0(4(1(2(2(z0))))) → 4(1(0(2(2(3(z0))))))
0(4(1(2(5(z0))))) → 3(4(1(0(2(5(z0))))))
0(4(2(1(2(z0))))) → 4(1(3(2(0(2(z0))))))
0(4(2(1(4(z0))))) → 0(2(1(4(4(4(z0))))))
0(4(2(5(2(z0))))) → 5(4(3(2(2(0(z0))))))
0(4(5(1(2(z0))))) → 1(4(2(0(5(5(z0))))))
0(4(5(1(2(z0))))) → 4(0(2(5(1(1(z0))))))
5(0(1(2(z0)))) → 1(3(2(5(0(z0)))))
5(0(1(2(z0)))) → 5(0(2(1(3(3(z0))))))
5(0(1(2(2(z0))))) → 5(0(2(2(1(2(z0))))))
5(0(2(4(2(z0))))) → 0(2(2(5(1(4(z0))))))
5(0(4(4(2(z0))))) → 0(5(2(5(4(4(z0))))))
Tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(1(2(z0))) → c1(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
S tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
K tuples:
0'(1(2(z0))) → c1(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(3(1(2(z0)))) → c25(0'(z0))
Defined Rule Symbols:
0, 5
Defined Pair Symbols:
0'
Compound Symbols:
c7, c25, c29, c38, c1, c10, c23, c15, c17, c18, c33, c40, c41
(19) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(1(2(5(z0)))) → c15(0'(z0))
We considered the (Usable) Rules:
5(0(4(4(2(z0))))) → 0(5(2(5(4(4(z0))))))
And the Tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(1(2(z0))) → c1(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0(x1)) = 0
POL(0'(x1)) = [2]x1
POL(1(x1)) = [2] + x1
POL(2(x1)) = x1
POL(3(x1)) = x1
POL(4(x1)) = x1
POL(5(x1)) = x1
POL(c1(x1)) = x1
POL(c10(x1)) = x1
POL(c15(x1)) = x1
POL(c17(x1)) = x1
POL(c18(x1)) = x1
POL(c23(x1)) = x1
POL(c25(x1)) = x1
POL(c29(x1)) = x1
POL(c33(x1)) = x1
POL(c38(x1)) = x1
POL(c40(x1)) = x1
POL(c41(x1)) = x1
POL(c7(x1)) = x1
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(1(3(2(z0))))
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(2(2(1(z0))))
0(1(2(z0))) → 0(2(2(1(4(z0)))))
0(1(2(z0))) → 5(1(0(5(2(3(z0))))))
0(2(4(z0))) → 0(2(1(4(3(z0)))))
0(4(2(z0))) → 4(0(2(3(z0))))
0(4(2(z0))) → 4(0(5(5(2(z0)))))
0(0(4(2(z0)))) → 0(0(2(2(3(4(z0))))))
0(1(2(2(z0)))) → 0(2(1(0(2(z0)))))
0(1(2(2(z0)))) → 1(3(0(2(2(z0)))))
0(1(2(4(z0)))) → 0(1(4(2(3(z0)))))
0(1(2(4(z0)))) → 4(0(2(2(1(1(z0))))))
0(1(2(4(z0)))) → 4(0(5(5(2(1(z0))))))
0(1(2(5(z0)))) → 3(5(5(2(1(0(z0))))))
0(1(4(2(z0)))) → 0(5(2(1(4(z0)))))
0(1(5(2(z0)))) → 1(5(0(2(3(z0)))))
0(1(5(2(z0)))) → 0(2(2(1(0(5(z0))))))
0(1(5(2(z0)))) → 5(5(0(2(1(3(z0))))))
0(2(4(2(z0)))) → 0(5(4(3(2(2(z0))))))
0(3(1(2(z0)))) → 0(2(1(3(2(z0)))))
0(3(1(2(z0)))) → 1(0(2(5(3(z0)))))
0(3(1(2(z0)))) → 1(5(0(2(3(z0)))))
0(3(1(2(z0)))) → 3(0(2(2(1(z0)))))
0(3(1(2(z0)))) → 3(2(2(1(0(z0)))))
0(3(1(2(z0)))) → 0(3(2(3(1(3(z0))))))
0(3(4(2(z0)))) → 0(2(2(3(4(z0)))))
0(1(1(2(5(z0))))) → 5(0(2(5(1(1(z0))))))
0(2(3(4(2(z0))))) → 3(2(2(3(4(0(z0))))))
0(3(1(2(5(z0))))) → 2(3(1(3(0(5(z0))))))
0(3(1(5(2(z0))))) → 0(3(2(5(1(2(z0))))))
0(3(4(1(4(z0))))) → 0(5(3(1(4(4(z0))))))
0(3(5(1(2(z0))))) → 5(5(3(2(1(0(z0))))))
0(4(0(4(2(z0))))) → 4(4(0(0(2(2(z0))))))
0(4(1(1(2(z0))))) → 3(1(4(0(2(1(z0))))))
0(4(1(2(2(z0))))) → 4(1(0(2(2(3(z0))))))
0(4(1(2(5(z0))))) → 3(4(1(0(2(5(z0))))))
0(4(2(1(2(z0))))) → 4(1(3(2(0(2(z0))))))
0(4(2(1(4(z0))))) → 0(2(1(4(4(4(z0))))))
0(4(2(5(2(z0))))) → 5(4(3(2(2(0(z0))))))
0(4(5(1(2(z0))))) → 1(4(2(0(5(5(z0))))))
0(4(5(1(2(z0))))) → 4(0(2(5(1(1(z0))))))
5(0(1(2(z0)))) → 1(3(2(5(0(z0)))))
5(0(1(2(z0)))) → 5(0(2(1(3(3(z0))))))
5(0(1(2(2(z0))))) → 5(0(2(2(1(2(z0))))))
5(0(2(4(2(z0))))) → 0(2(2(5(1(4(z0))))))
5(0(4(4(2(z0))))) → 0(5(2(5(4(4(z0))))))
Tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(1(2(z0))) → c1(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
S tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
K tuples:
0'(1(2(z0))) → c1(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(1(2(5(z0)))) → c15(0'(z0))
Defined Rule Symbols:
0, 5
Defined Pair Symbols:
0'
Compound Symbols:
c7, c25, c29, c38, c1, c10, c23, c15, c17, c18, c33, c40, c41
(21) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
0'(2(3(4(2(z0))))) → c29(0'(z0))
We considered the (Usable) Rules:
5(0(4(4(2(z0))))) → 0(5(2(5(4(4(z0))))))
And the Tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(1(2(z0))) → c1(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0(x1)) = 0
POL(0'(x1)) = [4]x1
POL(1(x1)) = x1
POL(2(x1)) = x1
POL(3(x1)) = x1
POL(4(x1)) = [1] + x1
POL(5(x1)) = x1
POL(c1(x1)) = x1
POL(c10(x1)) = x1
POL(c15(x1)) = x1
POL(c17(x1)) = x1
POL(c18(x1)) = x1
POL(c23(x1)) = x1
POL(c25(x1)) = x1
POL(c29(x1)) = x1
POL(c33(x1)) = x1
POL(c38(x1)) = x1
POL(c40(x1)) = x1
POL(c41(x1)) = x1
POL(c7(x1)) = x1
(22) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(1(3(2(z0))))
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(2(2(1(z0))))
0(1(2(z0))) → 0(2(2(1(4(z0)))))
0(1(2(z0))) → 5(1(0(5(2(3(z0))))))
0(2(4(z0))) → 0(2(1(4(3(z0)))))
0(4(2(z0))) → 4(0(2(3(z0))))
0(4(2(z0))) → 4(0(5(5(2(z0)))))
0(0(4(2(z0)))) → 0(0(2(2(3(4(z0))))))
0(1(2(2(z0)))) → 0(2(1(0(2(z0)))))
0(1(2(2(z0)))) → 1(3(0(2(2(z0)))))
0(1(2(4(z0)))) → 0(1(4(2(3(z0)))))
0(1(2(4(z0)))) → 4(0(2(2(1(1(z0))))))
0(1(2(4(z0)))) → 4(0(5(5(2(1(z0))))))
0(1(2(5(z0)))) → 3(5(5(2(1(0(z0))))))
0(1(4(2(z0)))) → 0(5(2(1(4(z0)))))
0(1(5(2(z0)))) → 1(5(0(2(3(z0)))))
0(1(5(2(z0)))) → 0(2(2(1(0(5(z0))))))
0(1(5(2(z0)))) → 5(5(0(2(1(3(z0))))))
0(2(4(2(z0)))) → 0(5(4(3(2(2(z0))))))
0(3(1(2(z0)))) → 0(2(1(3(2(z0)))))
0(3(1(2(z0)))) → 1(0(2(5(3(z0)))))
0(3(1(2(z0)))) → 1(5(0(2(3(z0)))))
0(3(1(2(z0)))) → 3(0(2(2(1(z0)))))
0(3(1(2(z0)))) → 3(2(2(1(0(z0)))))
0(3(1(2(z0)))) → 0(3(2(3(1(3(z0))))))
0(3(4(2(z0)))) → 0(2(2(3(4(z0)))))
0(1(1(2(5(z0))))) → 5(0(2(5(1(1(z0))))))
0(2(3(4(2(z0))))) → 3(2(2(3(4(0(z0))))))
0(3(1(2(5(z0))))) → 2(3(1(3(0(5(z0))))))
0(3(1(5(2(z0))))) → 0(3(2(5(1(2(z0))))))
0(3(4(1(4(z0))))) → 0(5(3(1(4(4(z0))))))
0(3(5(1(2(z0))))) → 5(5(3(2(1(0(z0))))))
0(4(0(4(2(z0))))) → 4(4(0(0(2(2(z0))))))
0(4(1(1(2(z0))))) → 3(1(4(0(2(1(z0))))))
0(4(1(2(2(z0))))) → 4(1(0(2(2(3(z0))))))
0(4(1(2(5(z0))))) → 3(4(1(0(2(5(z0))))))
0(4(2(1(2(z0))))) → 4(1(3(2(0(2(z0))))))
0(4(2(1(4(z0))))) → 0(2(1(4(4(4(z0))))))
0(4(2(5(2(z0))))) → 5(4(3(2(2(0(z0))))))
0(4(5(1(2(z0))))) → 1(4(2(0(5(5(z0))))))
0(4(5(1(2(z0))))) → 4(0(2(5(1(1(z0))))))
5(0(1(2(z0)))) → 1(3(2(5(0(z0)))))
5(0(1(2(z0)))) → 5(0(2(1(3(3(z0))))))
5(0(1(2(2(z0))))) → 5(0(2(2(1(2(z0))))))
5(0(2(4(2(z0))))) → 0(2(2(5(1(4(z0))))))
5(0(4(4(2(z0))))) → 0(5(2(5(4(4(z0))))))
Tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(1(2(z0))) → c1(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
S tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
K tuples:
0'(1(2(z0))) → c1(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
Defined Rule Symbols:
0, 5
Defined Pair Symbols:
0'
Compound Symbols:
c7, c25, c29, c38, c1, c10, c23, c15, c17, c18, c33, c40, c41
(23) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
We considered the (Usable) Rules:
5(0(4(4(2(z0))))) → 0(5(2(5(4(4(z0))))))
And the Tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(1(2(z0))) → c1(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0(x1)) = 0
POL(0'(x1)) = [4]x1
POL(1(x1)) = [1] + x1
POL(2(x1)) = x1
POL(3(x1)) = x1
POL(4(x1)) = x1
POL(5(x1)) = x1
POL(c1(x1)) = x1
POL(c10(x1)) = x1
POL(c15(x1)) = x1
POL(c17(x1)) = x1
POL(c18(x1)) = x1
POL(c23(x1)) = x1
POL(c25(x1)) = x1
POL(c29(x1)) = x1
POL(c33(x1)) = x1
POL(c38(x1)) = x1
POL(c40(x1)) = x1
POL(c41(x1)) = x1
POL(c7(x1)) = x1
(24) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(1(3(2(z0))))
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(2(2(1(z0))))
0(1(2(z0))) → 0(2(2(1(4(z0)))))
0(1(2(z0))) → 5(1(0(5(2(3(z0))))))
0(2(4(z0))) → 0(2(1(4(3(z0)))))
0(4(2(z0))) → 4(0(2(3(z0))))
0(4(2(z0))) → 4(0(5(5(2(z0)))))
0(0(4(2(z0)))) → 0(0(2(2(3(4(z0))))))
0(1(2(2(z0)))) → 0(2(1(0(2(z0)))))
0(1(2(2(z0)))) → 1(3(0(2(2(z0)))))
0(1(2(4(z0)))) → 0(1(4(2(3(z0)))))
0(1(2(4(z0)))) → 4(0(2(2(1(1(z0))))))
0(1(2(4(z0)))) → 4(0(5(5(2(1(z0))))))
0(1(2(5(z0)))) → 3(5(5(2(1(0(z0))))))
0(1(4(2(z0)))) → 0(5(2(1(4(z0)))))
0(1(5(2(z0)))) → 1(5(0(2(3(z0)))))
0(1(5(2(z0)))) → 0(2(2(1(0(5(z0))))))
0(1(5(2(z0)))) → 5(5(0(2(1(3(z0))))))
0(2(4(2(z0)))) → 0(5(4(3(2(2(z0))))))
0(3(1(2(z0)))) → 0(2(1(3(2(z0)))))
0(3(1(2(z0)))) → 1(0(2(5(3(z0)))))
0(3(1(2(z0)))) → 1(5(0(2(3(z0)))))
0(3(1(2(z0)))) → 3(0(2(2(1(z0)))))
0(3(1(2(z0)))) → 3(2(2(1(0(z0)))))
0(3(1(2(z0)))) → 0(3(2(3(1(3(z0))))))
0(3(4(2(z0)))) → 0(2(2(3(4(z0)))))
0(1(1(2(5(z0))))) → 5(0(2(5(1(1(z0))))))
0(2(3(4(2(z0))))) → 3(2(2(3(4(0(z0))))))
0(3(1(2(5(z0))))) → 2(3(1(3(0(5(z0))))))
0(3(1(5(2(z0))))) → 0(3(2(5(1(2(z0))))))
0(3(4(1(4(z0))))) → 0(5(3(1(4(4(z0))))))
0(3(5(1(2(z0))))) → 5(5(3(2(1(0(z0))))))
0(4(0(4(2(z0))))) → 4(4(0(0(2(2(z0))))))
0(4(1(1(2(z0))))) → 3(1(4(0(2(1(z0))))))
0(4(1(2(2(z0))))) → 4(1(0(2(2(3(z0))))))
0(4(1(2(5(z0))))) → 3(4(1(0(2(5(z0))))))
0(4(2(1(2(z0))))) → 4(1(3(2(0(2(z0))))))
0(4(2(1(4(z0))))) → 0(2(1(4(4(4(z0))))))
0(4(2(5(2(z0))))) → 5(4(3(2(2(0(z0))))))
0(4(5(1(2(z0))))) → 1(4(2(0(5(5(z0))))))
0(4(5(1(2(z0))))) → 4(0(2(5(1(1(z0))))))
5(0(1(2(z0)))) → 1(3(2(5(0(z0)))))
5(0(1(2(z0)))) → 5(0(2(1(3(3(z0))))))
5(0(1(2(2(z0))))) → 5(0(2(2(1(2(z0))))))
5(0(2(4(2(z0))))) → 0(2(2(5(1(4(z0))))))
5(0(4(4(2(z0))))) → 0(5(2(5(4(4(z0))))))
Tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(1(2(z0))) → c1(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
S tuples:
0'(4(2(z0))) → c7(0'(2(3(z0))))
K tuples:
0'(1(2(z0))) → c1(0'(z0))
0'(4(2(5(2(z0))))) → c40(0'(z0))
0'(4(2(1(2(z0))))) → c38(0'(2(z0)))
0'(3(1(2(z0)))) → c23(0'(2(3(z0))))
0'(1(5(2(z0)))) → c18(0'(5(z0)))
0'(1(5(2(z0)))) → c17(0'(2(3(z0))))
0'(3(5(1(2(z0))))) → c33(0'(z0))
0'(3(1(2(z0)))) → c25(0'(z0))
0'(1(2(2(z0)))) → c10(0'(2(z0)))
0'(1(2(5(z0)))) → c15(0'(z0))
0'(2(3(4(2(z0))))) → c29(0'(z0))
0'(4(5(1(2(z0))))) → c41(0'(5(5(z0))))
Defined Rule Symbols:
0, 5
Defined Pair Symbols:
0'
Compound Symbols:
c7, c25, c29, c38, c1, c10, c23, c15, c17, c18, c33, c40, c41
(25) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
0'(4(2(z0))) → c7(0'(2(3(z0))))
0'(2(3(4(2(z0))))) → c29(0'(z0))
Now S is empty
(26) BOUNDS(O(1), O(1))